($\lambda$$A$,$l$,$z$. hd($l$)) $\in$ $A$:Type$\rightarrow$$A$ List$^{+}\rightarrow\downarrow$True$\rightarrow$$A$